Inference at * 
Iof proof for Lemma fincr formation:


  FIncr 

latex

 by Unfold `fincr` 0 

latex

 1: 

 1:   {f | i:  if (i = 0) then  else {f(i - 1)...} fi }
 .

Definitions

FIncr